Inference at * 1 4 
Iof proof for Lemma fincr wf:

.....eq aux..... NILNIL

1. i : 
2. f : {f | i:{z:| z (i,j. i < j) i}   if (i = 0) then  else {f(i - 1)...} fi }
  if (i = 0) then  else {f(i - 1)...} fi   Type 

latex

 by ((AbReduce (-1)) 
CollapseTHEN (Assert j:{k:| k < i} . f(j)  )) 

latex

C1: .....assertion..... NILNIL

C1: 2. f : {f | i:{z:| z < i}   if (i = 0) then  else {f(i - 1)...} fi }
C1:   j:{k:| k < i} . f(j)  
C2: 

C2: 2. f : {f | i:{z:| z < i}   if (i = 0) then  else {f(i - 1)...} fi }
C2: 3. j:{k:| k < i} . f(j)  
C2:   if (i = 0) then  else {f(i - 1)...} fi   Type
C.

Definitions

x f y